$\forall$${\it es}$:ES, $e_{1}$, $e_{2}$:E, $P$:(discrete state@loc($e_{1}$)$\rightarrow\mathbb{P}$).
\\[0ex]$\forall$$e$$\in$[$e_{1}$,$e_{2}$).$P$((discrete state after $e$)) $\Leftarrow\!\Rightarrow$ $\forall$$e$$\in$($e_{1}$,$e_{2}$].$P$((discrete state when $e$))